Nuprl Lemma : mlnk_wf_d
11,40
postcript
pdf
D
:Dsys,
i
:Id,
m
:M(
i
).Msg. mlnk(
m
)
IdLnk
latex
Definitions
x
:
A
.
B
(
x
)
,
t
T
,
mlnk(
m
)
,
t
.1
,
M
.Msg
,
Msg(
da
)
,
Msg(
M
)
Lemmas
ma-msg
wf
,
d-m
wf
,
Id
wf
,
dsys
wf
origin
D:Dsys, i:Id, m:M(i).Msg. mlnk(m) 
IdLnk D:Dsys, i:Id, m:M(i).Msg. mlnk(m) IdLnk x:A. B(x) T